『抽象によるソフトウェア設計 Alloyではじめる形式手法』

演算子系

Q. <:

Q, :>

Q. ~

Q. ^

1章 はじめに

2章 ざっと一巡り

3章 論理系

one, lone, some

# で濃度

4章 言語

自分が自身の祖父

sig, フィールド

モデル図 run等ででる図

型と型検査

assert, fact, fun, pred

run for

module

5章 解析

6章 事例

リーダー選出

ホテルの問題

メディアの資産管理

メモリの抽象化

付録A 練習問題

付録B Alloy 言語リファレンス

付録C 中核の意味論

付録D 図的手法

付録E Alloy以外の手法

付録F Alloy Analyzer クイックガイド

付録G 訳語一覧

参考文献

訳者あとがき